# ATerm parser
# Purpose: Parse an ATerm into a Python tree of class ATerm
# Author:  Wouter Caarls
# Date:    05-11-2004

import sys, string, re

class ATerm:
  """ATerm class. The data type contains "data": the "name" of the
     ATerm node; "children", child ATerms, and "annotations", more
     child ATerms."""
  def __init__(self, data=None, children=[], annotations=[]):
    """Constructor"""
    self.data = data
    self.children = children
    self.annotations = annotations

  def __repr__(self, depth=0):
    """Print the ATerms in a programmer-friendly format: indented"""
    s = ""
    depth = depth + 1

    if self.data[0] == "\"":
      # String
      s = s + self.data
    elif self.data == "[]":
      # List
      s = s + "["
      if self.children != []:
        s = s + string.join(map(ATerm.__repr__, self.children,
                                _replicate(depth, len(self.children))),
                            ",\n" + depth * " ")
      s = s + "]"
    elif self.data == "()":
      # Tuple
      s = s + "("
      if self.children != []:
        s = s + string.join(map(ATerm.__repr__, self.children,
                                _replicate(depth, len(self.children))),
                            ",\n" + depth * " ")
      s = s + ")"
    else:
      # Ordinary
      s = s + str(self.data)
      depth = depth + len(str(self.data))
      if self.children != []:
        # Function application
        s = s + "("
        s = s + string.join(map(ATerm.__repr__, self.children,
                                _replicate(depth, len(self.children))),
                            ",\n" + depth * " ")
        s = s + ")"
    
    if self.annotations != []:
      s = s + " {" + string.join(map(ATerm.__repr__, self.annotations,
                                     _replicate(depth, len(self.annotations))),
                                 ", ") + "}"

    return s

  def __str__(self):
    return self.mystr(True)

  def __str_noannos__(self):
    return self.mystr(False)

  def mystr(self, withAnnos):
    """Print the ATerms in a program-friendly format: on one line"""
    if self.data[0] == "\"":
      # String
      s = self.data
    elif self.data == "[]":
      # List
      if withAnnos:
        s = "[" + string.join(map(ATerm.__str__, self.children), ",") + "]"
      else:
        s = "[" + string.join(map(ATerm.__str_noannos__, self.children), ",") + "]"      
    elif self.data == "()":
      # Tuple
      if withAnnos:
        s = "(" + string.join(map(ATerm.__str__, self.children), ",") + ")"
      else:
        s = "(" + string.join(map(ATerm.__str_noannos__, self.children), ",") + ")"
    else:
      # Ordinary
      s = self.data
      if self.children != []:
        # Function application
        if withAnnos:
          s = s + "(" + string.join(map(ATerm.__str__, self.children), ",") + ")"
        else:
          s = s + "(" + string.join(map(ATerm.__str_noannos__, self.children), ",") + ")"
    
    if withAnnos == True and self.annotations:
      s = s + " {" + string.join(map(ATerm.__str__, self.annotations), ",") + "}"

    return s

  def __eq__(self, other):
    try:
      return self.__str_noannos__() == other.__str_noannos__()
    except:
      return False

  def __hash__(self):
    return self.__str_noannos__().__hash__()

  def __ne__(self, other):
    return not (self == other)

  def evaluate(self):
    if self.data == "IntConst":
      return int(self.children[0].data[1:-1])
    elif self.data == "Negative":
      return -self.children[0].evaluate()
    elif self.data == "Add":
      return self.children[0].evaluate()+self.children[1].evaluate()
    elif self.data == "Subt":
      return self.children[0].evaluate()-self.children[1].evaluate()
    elif self.data == "Mul":
      return self.children[0].evaluate()*self.children[1].evaluate()
    elif self.data == "Div":
      return int(self.children[0].evaluate()/self.children[1].evaluate())
    else:
      raise "Not a constant expression (data %s)" % (self.data)

def ParseATerm(stringterm):
  """Parse a string into an ATerm. This is the only exported function."""
  global _c, _s

  _c = 0
  _s = stringterm
  _SkipLayout()

  if _EOS():
    return None

  return _ParseTerm()

def _SkipLayout():
  """Skip until string is empty or a no-layout character"""
  global _c, _s

  try:
    while _s[_c] in " \t":
      _c = _c + 1
  except IndexError:
    pass

def _SkipNextLayout():
  """Skip next character, then skip layout"""
  global _c

  _c = _c + 1
  _SkipLayout()

def _ParseTerm():
  """Parse a term. Index is the start of a valid term"""
  global _c, _s

  if _s[_c] == '"':
    # String
    _SkipNextLayout()
    term = _ParseStringTerm()
    if _EOS() or _s[_c] != '"':
      _RaiseError(SyntaxError, "Expected: '\"'")
    _SkipNextLayout()
    result = ATerm("\"" + term + "\"")
  elif _s[_c] == '[':
    # List
    _SkipNextLayout()
    terms = _ParseTerms()
    if _EOS() or _s[_c] != ']':
      _RaiseError(SyntaxError, "Expected: ']'")
    _SkipNextLayout()
    result = ATerm("[]", terms)
  elif _s[_c] == '(':
    # Tuple
    _SkipNextLayout()
    terms = _ParseTerms()
    if _EOS() or _s[_c] != ')':
      _RaiseError(SyntaxError, "Expected: ')'")
    _SkipNextLayout()
    result = ATerm("()", terms)
  else:
    # Ordinary term
    try:
      data = re.match("[^()\"\\[\\]{}, \t]+", _s[_c:]).group()
    except AttributeError:
      _RaiseError(SyntaxError, "Expected: term")
    _c = _c + len(data)
    _SkipLayout()
    result = ATerm(data)

  if _EOS():
    return result
  
  if _s[_c] == '(':
    # Function application
    _SkipNextLayout()
    terms = _ParseTerms()
    if _EOS() or _s[_c] != ')':
      _RaiseError(SyntaxError, "Expected: ')'")
    _SkipNextLayout()
    result.children = terms
  
  if _EOS():
    return result

  if _s[_c] == '{':
    # Annotations
    _SkipNextLayout()
    terms = _ParseTerms()
    if _EOS() or _s[_c] != '}':
      _RaiseError(SyntaxError, "Expected: '}'")
    _SkipNextLayout()
    result.annotations = terms
  
  return result

def _ParseStringTerm():
  """Parse a string. Index is at the first character of the string
     Parsing consists of consuming tokens until a " is found, but
     taking escapes into account""" 
  global _c, _s

  cold = _c

  while 1:
    if _EOS():
      # String empty before end of string
      raise SyntaxError, "Unterminated string constant"

    if _s[_c] == '\\':
      # Escape, skip next character
      _c = _c + 2
    elif _s[_c] == '\"':
      # End of string
      break
    else:
      # Consume character
      _c = _c + 1

  return _s[cold:_c]

def _ParseTerms():
  """Parse a list of terms, separated by commas"""
  global _c, _s

  try:
    terms = [_ParseTerm()]
  except SyntaxError:
    # Empty list of terms
    return []

  if _EOS():
    # Only one term
    return terms

  while _s[_c] == ',':
    _SkipNextLayout()
    terms.append(_ParseTerm())
    if _EOS():
      return terms

  return terms

def _RaiseError(e, s):
  """Raise a parse error, with a bit of helpful context"""
  toleft = min(_c, 10)
  left = _c - toleft
  right = _c + 10

  raise e, "column " + str(_c+1) + ": " + s + "\n" + \
        "..." + _s[left:right] + "...\n" + (toleft+3) * " " + "^\n"

def _EOS():
  """Check if the string is empty"""
  try:
    _s[_c]
  except IndexError:
    return True
  else:
    return False
  
def _replicate(o, c=1):
  """Replicate a character o c times"""
  l = [o]
  for i in range(c-1):
    l.append(o)
  return l

def getAnnotation(term, sought):
  for ann in term.annotations:
    if ann.data == sought:
      return ann.children[0]

  return None

sys.setrecursionlimit(8192);
_c = 0
_s = []
